update{-}spec(${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it kz}$:Knd$\times$Id fp$\rightarrow$ ($\mathbb{N}\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kz}$))$\rightarrow$${\it ds}$(2of(${\it kz}$))?Void)) List